* Step 1: Bounds WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: U101(mark(X1),X2,X3) -> mark(U101(X1,X2,X3)) U101(ok(X1),ok(X2),ok(X3)) -> ok(U101(X1,X2,X3)) U102(mark(X1),X2,X3) -> mark(U102(X1,X2,X3)) U102(ok(X1),ok(X2),ok(X3)) -> ok(U102(X1,X2,X3)) U103(mark(X1),X2,X3) -> mark(U103(X1,X2,X3)) U103(ok(X1),ok(X2),ok(X3)) -> ok(U103(X1,X2,X3)) U104(mark(X1),X2,X3) -> mark(U104(X1,X2,X3)) U104(ok(X1),ok(X2),ok(X3)) -> ok(U104(X1,X2,X3)) U105(mark(X1),X2) -> mark(U105(X1,X2)) U105(ok(X1),ok(X2)) -> ok(U105(X1,X2)) U106(mark(X)) -> mark(U106(X)) U106(ok(X)) -> ok(U106(X)) U11(mark(X1),X2,X3) -> mark(U11(X1,X2,X3)) U11(ok(X1),ok(X2),ok(X3)) -> ok(U11(X1,X2,X3)) U111(mark(X1),X2) -> mark(U111(X1,X2)) U111(ok(X1),ok(X2)) -> ok(U111(X1,X2)) U112(mark(X)) -> mark(U112(X)) U112(ok(X)) -> ok(U112(X)) U12(mark(X1),X2,X3) -> mark(U12(X1,X2,X3)) U12(ok(X1),ok(X2),ok(X3)) -> ok(U12(X1,X2,X3)) U121(mark(X1),X2) -> mark(U121(X1,X2)) U121(ok(X1),ok(X2)) -> ok(U121(X1,X2)) U122(mark(X)) -> mark(U122(X)) U122(ok(X)) -> ok(U122(X)) U13(mark(X1),X2,X3) -> mark(U13(X1,X2,X3)) U13(ok(X1),ok(X2),ok(X3)) -> ok(U13(X1,X2,X3)) U131(mark(X)) -> mark(U131(X)) U131(ok(X)) -> ok(U131(X)) U14(mark(X1),X2,X3) -> mark(U14(X1,X2,X3)) U14(ok(X1),ok(X2),ok(X3)) -> ok(U14(X1,X2,X3)) U141(mark(X)) -> mark(U141(X)) U141(ok(X)) -> ok(U141(X)) U151(mark(X)) -> mark(U151(X)) U151(ok(X)) -> ok(U151(X)) U161(mark(X)) -> mark(U161(X)) U161(ok(X)) -> ok(U161(X)) U171(mark(X1),X2) -> mark(U171(X1,X2)) U171(ok(X1),ok(X2)) -> ok(U171(X1,X2)) U172(mark(X)) -> mark(U172(X)) U172(ok(X)) -> ok(U172(X)) U181(mark(X1),X2) -> mark(U181(X1,X2)) U181(ok(X1),ok(X2)) -> ok(U181(X1,X2)) U182(mark(X1),X2) -> mark(U182(X1,X2)) U182(ok(X1),ok(X2)) -> ok(U182(X1,X2)) U183(mark(X)) -> mark(U183(X)) U183(ok(X)) -> ok(U183(X)) U191(mark(X1),X2) -> mark(U191(X1,X2)) U191(ok(X1),ok(X2)) -> ok(U191(X1,X2)) U192(mark(X1),X2) -> mark(U192(X1,X2)) U192(ok(X1),ok(X2)) -> ok(U192(X1,X2)) U193(mark(X)) -> mark(U193(X)) U193(ok(X)) -> ok(U193(X)) U201(mark(X1),X2,X3) -> mark(U201(X1,X2,X3)) U201(ok(X1),ok(X2),ok(X3)) -> ok(U201(X1,X2,X3)) U202(mark(X1),X2,X3) -> mark(U202(X1,X2,X3)) U202(ok(X1),ok(X2),ok(X3)) -> ok(U202(X1,X2,X3)) U203(mark(X1),X2,X3) -> mark(U203(X1,X2,X3)) U203(ok(X1),ok(X2),ok(X3)) -> ok(U203(X1,X2,X3)) U204(mark(X1),X2,X3) -> mark(U204(X1,X2,X3)) U204(ok(X1),ok(X2),ok(X3)) -> ok(U204(X1,X2,X3)) U205(mark(X1),X2) -> mark(U205(X1,X2)) U205(ok(X1),ok(X2)) -> ok(U205(X1,X2)) U206(mark(X)) -> mark(U206(X)) U206(ok(X)) -> ok(U206(X)) U21(mark(X1),X2,X3) -> mark(U21(X1,X2,X3)) U21(ok(X1),ok(X2),ok(X3)) -> ok(U21(X1,X2,X3)) U211(mark(X)) -> mark(U211(X)) U211(ok(X)) -> ok(U211(X)) U22(mark(X1),X2,X3) -> mark(U22(X1,X2,X3)) U22(ok(X1),ok(X2),ok(X3)) -> ok(U22(X1,X2,X3)) U221(mark(X)) -> mark(U221(X)) U221(ok(X)) -> ok(U221(X)) U23(mark(X1),X2,X3) -> mark(U23(X1,X2,X3)) U23(ok(X1),ok(X2),ok(X3)) -> ok(U23(X1,X2,X3)) U231(mark(X1),X2) -> mark(U231(X1,X2)) U231(ok(X1),ok(X2)) -> ok(U231(X1,X2)) U232(mark(X)) -> mark(U232(X)) U232(ok(X)) -> ok(U232(X)) U24(mark(X1),X2) -> mark(U24(X1,X2)) U24(ok(X1),ok(X2)) -> ok(U24(X1,X2)) U241(mark(X1),X2,X3) -> mark(U241(X1,X2,X3)) U241(ok(X1),ok(X2),ok(X3)) -> ok(U241(X1,X2,X3)) U242(mark(X1),X2,X3) -> mark(U242(X1,X2,X3)) U242(ok(X1),ok(X2),ok(X3)) -> ok(U242(X1,X2,X3)) U243(mark(X1),X2,X3) -> mark(U243(X1,X2,X3)) U243(ok(X1),ok(X2),ok(X3)) -> ok(U243(X1,X2,X3)) U244(mark(X1),X2,X3) -> mark(U244(X1,X2,X3)) U244(ok(X1),ok(X2),ok(X3)) -> ok(U244(X1,X2,X3)) U245(mark(X1),X2) -> mark(U245(X1,X2)) U245(ok(X1),ok(X2)) -> ok(U245(X1,X2)) U246(mark(X)) -> mark(U246(X)) U246(ok(X)) -> ok(U246(X)) U251(mark(X1),X2,X3) -> mark(U251(X1,X2,X3)) U251(ok(X1),ok(X2),ok(X3)) -> ok(U251(X1,X2,X3)) U252(mark(X1),X2,X3) -> mark(U252(X1,X2,X3)) U252(ok(X1),ok(X2),ok(X3)) -> ok(U252(X1,X2,X3)) U253(mark(X1),X2,X3) -> mark(U253(X1,X2,X3)) U253(ok(X1),ok(X2),ok(X3)) -> ok(U253(X1,X2,X3)) U254(mark(X1),X2,X3) -> mark(U254(X1,X2,X3)) U254(ok(X1),ok(X2),ok(X3)) -> ok(U254(X1,X2,X3)) U255(mark(X1),X2) -> mark(U255(X1,X2)) U255(ok(X1),ok(X2)) -> ok(U255(X1,X2)) U256(mark(X)) -> mark(U256(X)) U256(ok(X)) -> ok(U256(X)) U261(mark(X1),X2) -> mark(U261(X1,X2)) U261(ok(X1),ok(X2)) -> ok(U261(X1,X2)) U262(mark(X)) -> mark(U262(X)) U262(ok(X)) -> ok(U262(X)) U271(mark(X1),X2) -> mark(U271(X1,X2)) U271(ok(X1),ok(X2)) -> ok(U271(X1,X2)) U272(mark(X)) -> mark(U272(X)) U272(ok(X)) -> ok(U272(X)) U281(mark(X1),X2) -> mark(U281(X1,X2)) U281(ok(X1),ok(X2)) -> ok(U281(X1,X2)) U282(mark(X1),X2) -> mark(U282(X1,X2)) U282(ok(X1),ok(X2)) -> ok(U282(X1,X2)) U291(mark(X1),X2,X3) -> mark(U291(X1,X2,X3)) U291(ok(X1),ok(X2),ok(X3)) -> ok(U291(X1,X2,X3)) U292(mark(X1),X2,X3) -> mark(U292(X1,X2,X3)) U292(ok(X1),ok(X2),ok(X3)) -> ok(U292(X1,X2,X3)) U293(mark(X1),X2,X3) -> mark(U293(X1,X2,X3)) U293(ok(X1),ok(X2),ok(X3)) -> ok(U293(X1,X2,X3)) U294(mark(X1),X2,X3) -> mark(U294(X1,X2,X3)) U294(ok(X1),ok(X2),ok(X3)) -> ok(U294(X1,X2,X3)) U301(mark(X1),X2,X3) -> mark(U301(X1,X2,X3)) U301(ok(X1),ok(X2),ok(X3)) -> ok(U301(X1,X2,X3)) U302(mark(X1),X2) -> mark(U302(X1,X2)) U302(ok(X1),ok(X2)) -> ok(U302(X1,X2)) U303(mark(X1),X2) -> mark(U303(X1,X2)) U303(ok(X1),ok(X2)) -> ok(U303(X1,X2)) U304(mark(X1),X2) -> mark(U304(X1,X2)) U304(ok(X1),ok(X2)) -> ok(U304(X1,X2)) U31(mark(X1),X2,X3) -> mark(U31(X1,X2,X3)) U31(ok(X1),ok(X2),ok(X3)) -> ok(U31(X1,X2,X3)) U311(mark(X1),X2) -> mark(U311(X1,X2)) U311(ok(X1),ok(X2)) -> ok(U311(X1,X2)) U312(mark(X1),X2) -> mark(U312(X1,X2)) U312(ok(X1),ok(X2)) -> ok(U312(X1,X2)) U32(mark(X1),X2,X3) -> mark(U32(X1,X2,X3)) U32(ok(X1),ok(X2),ok(X3)) -> ok(U32(X1,X2,X3)) U321(mark(X1),X2,X3,X4) -> mark(U321(X1,X2,X3,X4)) U321(ok(X1),ok(X2),ok(X3),ok(X4)) -> ok(U321(X1,X2,X3,X4)) U322(mark(X1),X2,X3,X4) -> mark(U322(X1,X2,X3,X4)) U322(ok(X1),ok(X2),ok(X3),ok(X4)) -> ok(U322(X1,X2,X3,X4)) U323(mark(X1),X2,X3,X4) -> mark(U323(X1,X2,X3,X4)) U323(ok(X1),ok(X2),ok(X3),ok(X4)) -> ok(U323(X1,X2,X3,X4)) U324(mark(X1),X2,X3,X4) -> mark(U324(X1,X2,X3,X4)) U324(ok(X1),ok(X2),ok(X3),ok(X4)) -> ok(U324(X1,X2,X3,X4)) U325(mark(X1),X2,X3,X4) -> mark(U325(X1,X2,X3,X4)) U325(ok(X1),ok(X2),ok(X3),ok(X4)) -> ok(U325(X1,X2,X3,X4)) U326(mark(X1),X2,X3,X4) -> mark(U326(X1,X2,X3,X4)) U326(ok(X1),ok(X2),ok(X3),ok(X4)) -> ok(U326(X1,X2,X3,X4)) U327(mark(X1),X2) -> mark(U327(X1,X2)) U327(ok(X1),ok(X2)) -> ok(U327(X1,X2)) U33(mark(X1),X2,X3) -> mark(U33(X1,X2,X3)) U33(ok(X1),ok(X2),ok(X3)) -> ok(U33(X1,X2,X3)) U331(mark(X1),X2,X3) -> mark(U331(X1,X2,X3)) U331(ok(X1),ok(X2),ok(X3)) -> ok(U331(X1,X2,X3)) U332(mark(X1),X2) -> mark(U332(X1,X2)) U332(ok(X1),ok(X2)) -> ok(U332(X1,X2)) U333(mark(X1),X2) -> mark(U333(X1,X2)) U333(ok(X1),ok(X2)) -> ok(U333(X1,X2)) U334(mark(X1),X2) -> mark(U334(X1,X2)) U334(ok(X1),ok(X2)) -> ok(U334(X1,X2)) U34(mark(X1),X2) -> mark(U34(X1,X2)) U34(ok(X1),ok(X2)) -> ok(U34(X1,X2)) U341(mark(X1),X2,X3) -> mark(U341(X1,X2,X3)) U341(ok(X1),ok(X2),ok(X3)) -> ok(U341(X1,X2,X3)) U342(mark(X1),X2,X3) -> mark(U342(X1,X2,X3)) U342(ok(X1),ok(X2),ok(X3)) -> ok(U342(X1,X2,X3)) U343(mark(X1),X2,X3) -> mark(U343(X1,X2,X3)) U343(ok(X1),ok(X2),ok(X3)) -> ok(U343(X1,X2,X3)) U344(mark(X1),X2,X3) -> mark(U344(X1,X2,X3)) U344(ok(X1),ok(X2),ok(X3)) -> ok(U344(X1,X2,X3)) U41(mark(X1),X2,X3) -> mark(U41(X1,X2,X3)) U41(ok(X1),ok(X2),ok(X3)) -> ok(U41(X1,X2,X3)) U42(mark(X1),X2,X3) -> mark(U42(X1,X2,X3)) U42(ok(X1),ok(X2),ok(X3)) -> ok(U42(X1,X2,X3)) U43(mark(X1),X2,X3) -> mark(U43(X1,X2,X3)) U43(ok(X1),ok(X2),ok(X3)) -> ok(U43(X1,X2,X3)) U44(mark(X1),X2,X3) -> mark(U44(X1,X2,X3)) U44(ok(X1),ok(X2),ok(X3)) -> ok(U44(X1,X2,X3)) U45(mark(X1),X2) -> mark(U45(X1,X2)) U45(ok(X1),ok(X2)) -> ok(U45(X1,X2)) U46(mark(X)) -> mark(U46(X)) U46(ok(X)) -> ok(U46(X)) U51(mark(X1),X2,X3) -> mark(U51(X1,X2,X3)) U51(ok(X1),ok(X2),ok(X3)) -> ok(U51(X1,X2,X3)) U52(mark(X1),X2,X3) -> mark(U52(X1,X2,X3)) U52(ok(X1),ok(X2),ok(X3)) -> ok(U52(X1,X2,X3)) U53(mark(X1),X2,X3) -> mark(U53(X1,X2,X3)) U53(ok(X1),ok(X2),ok(X3)) -> ok(U53(X1,X2,X3)) U54(mark(X1),X2,X3) -> mark(U54(X1,X2,X3)) U54(ok(X1),ok(X2),ok(X3)) -> ok(U54(X1,X2,X3)) U55(mark(X1),X2) -> mark(U55(X1,X2)) U55(ok(X1),ok(X2)) -> ok(U55(X1,X2)) U56(mark(X)) -> mark(U56(X)) U56(ok(X)) -> ok(U56(X)) U61(mark(X1),X2) -> mark(U61(X1,X2)) U61(ok(X1),ok(X2)) -> ok(U61(X1,X2)) U62(mark(X1),X2) -> mark(U62(X1,X2)) U62(ok(X1),ok(X2)) -> ok(U62(X1,X2)) U63(mark(X)) -> mark(U63(X)) U63(ok(X)) -> ok(U63(X)) U71(mark(X1),X2) -> mark(U71(X1,X2)) U71(ok(X1),ok(X2)) -> ok(U71(X1,X2)) U72(mark(X1),X2) -> mark(U72(X1,X2)) U72(ok(X1),ok(X2)) -> ok(U72(X1,X2)) U73(mark(X)) -> mark(U73(X)) U73(ok(X)) -> ok(U73(X)) U81(mark(X1),X2) -> mark(U81(X1,X2)) U81(ok(X1),ok(X2)) -> ok(U81(X1,X2)) U82(mark(X1),X2) -> mark(U82(X1,X2)) U82(ok(X1),ok(X2)) -> ok(U82(X1,X2)) U83(mark(X)) -> mark(U83(X)) U83(ok(X)) -> ok(U83(X)) U91(mark(X1),X2) -> mark(U91(X1,X2)) U91(ok(X1),ok(X2)) -> ok(U91(X1,X2)) U92(mark(X1),X2) -> mark(U92(X1,X2)) U92(ok(X1),ok(X2)) -> ok(U92(X1,X2)) U93(mark(X)) -> mark(U93(X)) U93(ok(X)) -> ok(U93(X)) afterNth(X1,mark(X2)) -> mark(afterNth(X1,X2)) afterNth(mark(X1),X2) -> mark(afterNth(X1,X2)) afterNth(ok(X1),ok(X2)) -> ok(afterNth(X1,X2)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) fst(mark(X)) -> mark(fst(X)) fst(ok(X)) -> ok(fst(X)) head(mark(X)) -> mark(head(X)) head(ok(X)) -> ok(head(X)) isLNat(ok(X)) -> ok(isLNat(X)) isLNatKind(ok(X)) -> ok(isLNatKind(X)) isNatural(ok(X)) -> ok(isNatural(X)) isNaturalKind(ok(X)) -> ok(isNaturalKind(X)) isPLNat(ok(X)) -> ok(isPLNat(X)) isPLNatKind(ok(X)) -> ok(isPLNatKind(X)) natsFrom(mark(X)) -> mark(natsFrom(X)) natsFrom(ok(X)) -> ok(natsFrom(X)) pair(X1,mark(X2)) -> mark(pair(X1,X2)) pair(mark(X1),X2) -> mark(pair(X1,X2)) pair(ok(X1),ok(X2)) -> ok(pair(X1,X2)) proper(0()) -> ok(0()) proper(nil()) -> ok(nil()) proper(tt()) -> ok(tt()) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) snd(mark(X)) -> mark(snd(X)) snd(ok(X)) -> ok(snd(X)) splitAt(X1,mark(X2)) -> mark(splitAt(X1,X2)) splitAt(mark(X1),X2) -> mark(splitAt(X1,X2)) splitAt(ok(X1),ok(X2)) -> ok(splitAt(X1,X2)) tail(mark(X)) -> mark(tail(X)) tail(ok(X)) -> ok(tail(X)) take(X1,mark(X2)) -> mark(take(X1,X2)) take(mark(X1),X2) -> mark(take(X1,X2)) take(ok(X1),ok(X2)) -> ok(take(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) - Signature: {U101/3,U102/3,U103/3,U104/3,U105/2,U106/1,U11/3,U111/2,U112/1,U12/3,U121/2,U122/1,U13/3,U131/1,U14/3,U141/1 ,U151/1,U161/1,U171/2,U172/1,U181/2,U182/2,U183/1,U191/2,U192/2,U193/1,U201/3,U202/3,U203/3,U204/3,U205/2 ,U206/1,U21/3,U211/1,U22/3,U221/1,U23/3,U231/2,U232/1,U24/2,U241/3,U242/3,U243/3,U244/3,U245/2,U246/1,U251/3 ,U252/3,U253/3,U254/3,U255/2,U256/1,U261/2,U262/1,U271/2,U272/1,U281/2,U282/2,U291/3,U292/3,U293/3,U294/3 ,U301/3,U302/2,U303/2,U304/2,U31/3,U311/2,U312/2,U32/3,U321/4,U322/4,U323/4,U324/4,U325/4,U326/4,U327/2 ,U33/3,U331/3,U332/2,U333/2,U334/2,U34/2,U341/3,U342/3,U343/3,U344/3,U41/3,U42/3,U43/3,U44/3,U45/2,U46/1 ,U51/3,U52/3,U53/3,U54/3,U55/2,U56/1,U61/2,U62/2,U63/1,U71/2,U72/2,U73/1,U81/2,U82/2,U83/1,U91/2,U92/2,U93/1 ,afterNth/2,cons/2,fst/1,head/1,isLNat/1,isLNatKind/1,isNatural/1,isNaturalKind/1,isPLNat/1,isPLNatKind/1 ,natsFrom/1,pair/2,proper/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,top/1} / {0/0,active/1,mark/1,nil/0,ok/1 ,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {U101,U102,U103,U104,U105,U106,U11,U111,U112,U12,U121,U122 ,U13,U131,U14,U141,U151,U161,U171,U172,U181,U182,U183,U191,U192,U193,U201,U202,U203,U204,U205,U206,U21,U211 ,U22,U221,U23,U231,U232,U24,U241,U242,U243,U244,U245,U246,U251,U252,U253,U254,U255,U256,U261,U262,U271,U272 ,U281,U282,U291,U292,U293,U294,U301,U302,U303,U304,U31,U311,U312,U32,U321,U322,U323,U324,U325,U326,U327,U33 ,U331,U332,U333,U334,U34,U341,U342,U343,U344,U41,U42,U43,U44,U45,U46,U51,U52,U53,U54,U55,U56,U61,U62,U63,U71 ,U72,U73,U81,U82,U83,U91,U92,U93,afterNth,cons,fst,head,isLNat,isLNatKind,isNatural,isNaturalKind,isPLNat ,isPLNatKind,natsFrom,pair,proper,s,sel,snd,splitAt,tail,take,top} and constructors {0,active,mark,nil,ok ,tt} + Applied Processor: Bounds {initialAutomaton = minimal, enrichment = match} + Details: The problem is match-bounded by 2. The enriched problem is compatible with follwoing automaton. 0_0() -> 2 0_1() -> 3 U101_0(2,2,2) -> 1 U101_1(2,2,2) -> 3 U102_0(2,2,2) -> 1 U102_1(2,2,2) -> 3 U103_0(2,2,2) -> 1 U103_1(2,2,2) -> 3 U104_0(2,2,2) -> 1 U104_1(2,2,2) -> 3 U105_0(2,2) -> 1 U105_1(2,2) -> 3 U106_0(2) -> 1 U106_1(2) -> 3 U11_0(2,2,2) -> 1 U11_1(2,2,2) -> 3 U111_0(2,2) -> 1 U111_1(2,2) -> 3 U112_0(2) -> 1 U112_1(2) -> 3 U12_0(2,2,2) -> 1 U12_1(2,2,2) -> 3 U121_0(2,2) -> 1 U121_1(2,2) -> 3 U122_0(2) -> 1 U122_1(2) -> 3 U13_0(2,2,2) -> 1 U13_1(2,2,2) -> 3 U131_0(2) -> 1 U131_1(2) -> 3 U14_0(2,2,2) -> 1 U14_1(2,2,2) -> 3 U141_0(2) -> 1 U141_1(2) -> 3 U151_0(2) -> 1 U151_1(2) -> 3 U161_0(2) -> 1 U161_1(2) -> 3 U171_0(2,2) -> 1 U171_1(2,2) -> 3 U172_0(2) -> 1 U172_1(2) -> 3 U181_0(2,2) -> 1 U181_1(2,2) -> 3 U182_0(2,2) -> 1 U182_1(2,2) -> 3 U183_0(2) -> 1 U183_1(2) -> 3 U191_0(2,2) -> 1 U191_1(2,2) -> 3 U192_0(2,2) -> 1 U192_1(2,2) -> 3 U193_0(2) -> 1 U193_1(2) -> 3 U201_0(2,2,2) -> 1 U201_1(2,2,2) -> 3 U202_0(2,2,2) -> 1 U202_1(2,2,2) -> 3 U203_0(2,2,2) -> 1 U203_1(2,2,2) -> 3 U204_0(2,2,2) -> 1 U204_1(2,2,2) -> 3 U205_0(2,2) -> 1 U205_1(2,2) -> 3 U206_0(2) -> 1 U206_1(2) -> 3 U21_0(2,2,2) -> 1 U21_1(2,2,2) -> 3 U211_0(2) -> 1 U211_1(2) -> 3 U22_0(2,2,2) -> 1 U22_1(2,2,2) -> 3 U221_0(2) -> 1 U221_1(2) -> 3 U23_0(2,2,2) -> 1 U23_1(2,2,2) -> 3 U231_0(2,2) -> 1 U231_1(2,2) -> 3 U232_0(2) -> 1 U232_1(2) -> 3 U24_0(2,2) -> 1 U24_1(2,2) -> 3 U241_0(2,2,2) -> 1 U241_1(2,2,2) -> 3 U242_0(2,2,2) -> 1 U242_1(2,2,2) -> 3 U243_0(2,2,2) -> 1 U243_1(2,2,2) -> 3 U244_0(2,2,2) -> 1 U244_1(2,2,2) -> 3 U245_0(2,2) -> 1 U245_1(2,2) -> 3 U246_0(2) -> 1 U246_1(2) -> 3 U251_0(2,2,2) -> 1 U251_1(2,2,2) -> 3 U252_0(2,2,2) -> 1 U252_1(2,2,2) -> 3 U253_0(2,2,2) -> 1 U253_1(2,2,2) -> 3 U254_0(2,2,2) -> 1 U254_1(2,2,2) -> 3 U255_0(2,2) -> 1 U255_1(2,2) -> 3 U256_0(2) -> 1 U256_1(2) -> 3 U261_0(2,2) -> 1 U261_1(2,2) -> 3 U262_0(2) -> 1 U262_1(2) -> 3 U271_0(2,2) -> 1 U271_1(2,2) -> 3 U272_0(2) -> 1 U272_1(2) -> 3 U281_0(2,2) -> 1 U281_1(2,2) -> 3 U282_0(2,2) -> 1 U282_1(2,2) -> 3 U291_0(2,2,2) -> 1 U291_1(2,2,2) -> 3 U292_0(2,2,2) -> 1 U292_1(2,2,2) -> 3 U293_0(2,2,2) -> 1 U293_1(2,2,2) -> 3 U294_0(2,2,2) -> 1 U294_1(2,2,2) -> 3 U301_0(2,2,2) -> 1 U301_1(2,2,2) -> 3 U302_0(2,2) -> 1 U302_1(2,2) -> 3 U303_0(2,2) -> 1 U303_1(2,2) -> 3 U304_0(2,2) -> 1 U304_1(2,2) -> 3 U31_0(2,2,2) -> 1 U31_1(2,2,2) -> 3 U311_0(2,2) -> 1 U311_1(2,2) -> 3 U312_0(2,2) -> 1 U312_1(2,2) -> 3 U32_0(2,2,2) -> 1 U32_1(2,2,2) -> 3 U321_0(2,2,2,2) -> 1 U321_1(2,2,2,2) -> 3 U322_0(2,2,2,2) -> 1 U322_1(2,2,2,2) -> 3 U323_0(2,2,2,2) -> 1 U323_1(2,2,2,2) -> 3 U324_0(2,2,2,2) -> 1 U324_1(2,2,2,2) -> 3 U325_0(2,2,2,2) -> 1 U325_1(2,2,2,2) -> 3 U326_0(2,2,2,2) -> 1 U326_1(2,2,2,2) -> 3 U327_0(2,2) -> 1 U327_1(2,2) -> 3 U33_0(2,2,2) -> 1 U33_1(2,2,2) -> 3 U331_0(2,2,2) -> 1 U331_1(2,2,2) -> 3 U332_0(2,2) -> 1 U332_1(2,2) -> 3 U333_0(2,2) -> 1 U333_1(2,2) -> 3 U334_0(2,2) -> 1 U334_1(2,2) -> 3 U34_0(2,2) -> 1 U34_1(2,2) -> 3 U341_0(2,2,2) -> 1 U341_1(2,2,2) -> 3 U342_0(2,2,2) -> 1 U342_1(2,2,2) -> 3 U343_0(2,2,2) -> 1 U343_1(2,2,2) -> 3 U344_0(2,2,2) -> 1 U344_1(2,2,2) -> 3 U41_0(2,2,2) -> 1 U41_1(2,2,2) -> 3 U42_0(2,2,2) -> 1 U42_1(2,2,2) -> 3 U43_0(2,2,2) -> 1 U43_1(2,2,2) -> 3 U44_0(2,2,2) -> 1 U44_1(2,2,2) -> 3 U45_0(2,2) -> 1 U45_1(2,2) -> 3 U46_0(2) -> 1 U46_1(2) -> 3 U51_0(2,2,2) -> 1 U51_1(2,2,2) -> 3 U52_0(2,2,2) -> 1 U52_1(2,2,2) -> 3 U53_0(2,2,2) -> 1 U53_1(2,2,2) -> 3 U54_0(2,2,2) -> 1 U54_1(2,2,2) -> 3 U55_0(2,2) -> 1 U55_1(2,2) -> 3 U56_0(2) -> 1 U56_1(2) -> 3 U61_0(2,2) -> 1 U61_1(2,2) -> 3 U62_0(2,2) -> 1 U62_1(2,2) -> 3 U63_0(2) -> 1 U63_1(2) -> 3 U71_0(2,2) -> 1 U71_1(2,2) -> 3 U72_0(2,2) -> 1 U72_1(2,2) -> 3 U73_0(2) -> 1 U73_1(2) -> 3 U81_0(2,2) -> 1 U81_1(2,2) -> 3 U82_0(2,2) -> 1 U82_1(2,2) -> 3 U83_0(2) -> 1 U83_1(2) -> 3 U91_0(2,2) -> 1 U91_1(2,2) -> 3 U92_0(2,2) -> 1 U92_1(2,2) -> 3 U93_0(2) -> 1 U93_1(2) -> 3 active_0(2) -> 2 active_1(2) -> 4 active_2(3) -> 5 afterNth_0(2,2) -> 1 afterNth_1(2,2) -> 3 cons_0(2,2) -> 1 cons_1(2,2) -> 3 fst_0(2) -> 1 fst_1(2) -> 3 head_0(2) -> 1 head_1(2) -> 3 isLNat_0(2) -> 1 isLNat_1(2) -> 3 isLNatKind_0(2) -> 1 isLNatKind_1(2) -> 3 isNatural_0(2) -> 1 isNatural_1(2) -> 3 isNaturalKind_0(2) -> 1 isNaturalKind_1(2) -> 3 isPLNat_0(2) -> 1 isPLNat_1(2) -> 3 isPLNatKind_0(2) -> 1 isPLNatKind_1(2) -> 3 mark_0(2) -> 2 mark_1(3) -> 1 mark_1(3) -> 3 natsFrom_0(2) -> 1 natsFrom_1(2) -> 3 nil_0() -> 2 nil_1() -> 3 ok_0(2) -> 2 ok_1(3) -> 1 ok_1(3) -> 3 ok_1(3) -> 4 pair_0(2,2) -> 1 pair_1(2,2) -> 3 proper_0(2) -> 1 proper_1(2) -> 4 s_0(2) -> 1 s_1(2) -> 3 sel_0(2,2) -> 1 sel_1(2,2) -> 3 snd_0(2) -> 1 snd_1(2) -> 3 splitAt_0(2,2) -> 1 splitAt_1(2,2) -> 3 tail_0(2) -> 1 tail_1(2) -> 3 take_0(2,2) -> 1 take_1(2,2) -> 3 top_0(2) -> 1 top_1(4) -> 1 top_2(5) -> 1 tt_0() -> 2 tt_1() -> 3 * Step 2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: U101(mark(X1),X2,X3) -> mark(U101(X1,X2,X3)) U101(ok(X1),ok(X2),ok(X3)) -> ok(U101(X1,X2,X3)) U102(mark(X1),X2,X3) -> mark(U102(X1,X2,X3)) U102(ok(X1),ok(X2),ok(X3)) -> ok(U102(X1,X2,X3)) U103(mark(X1),X2,X3) -> mark(U103(X1,X2,X3)) U103(ok(X1),ok(X2),ok(X3)) -> ok(U103(X1,X2,X3)) U104(mark(X1),X2,X3) -> mark(U104(X1,X2,X3)) U104(ok(X1),ok(X2),ok(X3)) -> ok(U104(X1,X2,X3)) U105(mark(X1),X2) -> mark(U105(X1,X2)) U105(ok(X1),ok(X2)) -> ok(U105(X1,X2)) U106(mark(X)) -> mark(U106(X)) U106(ok(X)) -> ok(U106(X)) U11(mark(X1),X2,X3) -> mark(U11(X1,X2,X3)) U11(ok(X1),ok(X2),ok(X3)) -> ok(U11(X1,X2,X3)) U111(mark(X1),X2) -> mark(U111(X1,X2)) U111(ok(X1),ok(X2)) -> ok(U111(X1,X2)) U112(mark(X)) -> mark(U112(X)) U112(ok(X)) -> ok(U112(X)) U12(mark(X1),X2,X3) -> mark(U12(X1,X2,X3)) U12(ok(X1),ok(X2),ok(X3)) -> ok(U12(X1,X2,X3)) U121(mark(X1),X2) -> mark(U121(X1,X2)) U121(ok(X1),ok(X2)) -> ok(U121(X1,X2)) U122(mark(X)) -> mark(U122(X)) U122(ok(X)) -> ok(U122(X)) U13(mark(X1),X2,X3) -> mark(U13(X1,X2,X3)) U13(ok(X1),ok(X2),ok(X3)) -> ok(U13(X1,X2,X3)) U131(mark(X)) -> mark(U131(X)) U131(ok(X)) -> ok(U131(X)) U14(mark(X1),X2,X3) -> mark(U14(X1,X2,X3)) U14(ok(X1),ok(X2),ok(X3)) -> ok(U14(X1,X2,X3)) U141(mark(X)) -> mark(U141(X)) U141(ok(X)) -> ok(U141(X)) U151(mark(X)) -> mark(U151(X)) U151(ok(X)) -> ok(U151(X)) U161(mark(X)) -> mark(U161(X)) U161(ok(X)) -> ok(U161(X)) U171(mark(X1),X2) -> mark(U171(X1,X2)) U171(ok(X1),ok(X2)) -> ok(U171(X1,X2)) U172(mark(X)) -> mark(U172(X)) U172(ok(X)) -> ok(U172(X)) U181(mark(X1),X2) -> mark(U181(X1,X2)) U181(ok(X1),ok(X2)) -> ok(U181(X1,X2)) U182(mark(X1),X2) -> mark(U182(X1,X2)) U182(ok(X1),ok(X2)) -> ok(U182(X1,X2)) U183(mark(X)) -> mark(U183(X)) U183(ok(X)) -> ok(U183(X)) U191(mark(X1),X2) -> mark(U191(X1,X2)) U191(ok(X1),ok(X2)) -> ok(U191(X1,X2)) U192(mark(X1),X2) -> mark(U192(X1,X2)) U192(ok(X1),ok(X2)) -> ok(U192(X1,X2)) U193(mark(X)) -> mark(U193(X)) U193(ok(X)) -> ok(U193(X)) U201(mark(X1),X2,X3) -> mark(U201(X1,X2,X3)) U201(ok(X1),ok(X2),ok(X3)) -> ok(U201(X1,X2,X3)) U202(mark(X1),X2,X3) -> mark(U202(X1,X2,X3)) U202(ok(X1),ok(X2),ok(X3)) -> ok(U202(X1,X2,X3)) U203(mark(X1),X2,X3) -> mark(U203(X1,X2,X3)) U203(ok(X1),ok(X2),ok(X3)) -> ok(U203(X1,X2,X3)) U204(mark(X1),X2,X3) -> mark(U204(X1,X2,X3)) U204(ok(X1),ok(X2),ok(X3)) -> ok(U204(X1,X2,X3)) U205(mark(X1),X2) -> mark(U205(X1,X2)) U205(ok(X1),ok(X2)) -> ok(U205(X1,X2)) U206(mark(X)) -> mark(U206(X)) U206(ok(X)) -> ok(U206(X)) U21(mark(X1),X2,X3) -> mark(U21(X1,X2,X3)) U21(ok(X1),ok(X2),ok(X3)) -> ok(U21(X1,X2,X3)) U211(mark(X)) -> mark(U211(X)) U211(ok(X)) -> ok(U211(X)) U22(mark(X1),X2,X3) -> mark(U22(X1,X2,X3)) U22(ok(X1),ok(X2),ok(X3)) -> ok(U22(X1,X2,X3)) U221(mark(X)) -> mark(U221(X)) U221(ok(X)) -> ok(U221(X)) U23(mark(X1),X2,X3) -> mark(U23(X1,X2,X3)) U23(ok(X1),ok(X2),ok(X3)) -> ok(U23(X1,X2,X3)) U231(mark(X1),X2) -> mark(U231(X1,X2)) U231(ok(X1),ok(X2)) -> ok(U231(X1,X2)) U232(mark(X)) -> mark(U232(X)) U232(ok(X)) -> ok(U232(X)) U24(mark(X1),X2) -> mark(U24(X1,X2)) U24(ok(X1),ok(X2)) -> ok(U24(X1,X2)) U241(mark(X1),X2,X3) -> mark(U241(X1,X2,X3)) U241(ok(X1),ok(X2),ok(X3)) -> ok(U241(X1,X2,X3)) U242(mark(X1),X2,X3) -> mark(U242(X1,X2,X3)) U242(ok(X1),ok(X2),ok(X3)) -> ok(U242(X1,X2,X3)) U243(mark(X1),X2,X3) -> mark(U243(X1,X2,X3)) U243(ok(X1),ok(X2),ok(X3)) -> ok(U243(X1,X2,X3)) U244(mark(X1),X2,X3) -> mark(U244(X1,X2,X3)) U244(ok(X1),ok(X2),ok(X3)) -> ok(U244(X1,X2,X3)) U245(mark(X1),X2) -> mark(U245(X1,X2)) U245(ok(X1),ok(X2)) -> ok(U245(X1,X2)) U246(mark(X)) -> mark(U246(X)) U246(ok(X)) -> ok(U246(X)) U251(mark(X1),X2,X3) -> mark(U251(X1,X2,X3)) U251(ok(X1),ok(X2),ok(X3)) -> ok(U251(X1,X2,X3)) U252(mark(X1),X2,X3) -> mark(U252(X1,X2,X3)) U252(ok(X1),ok(X2),ok(X3)) -> ok(U252(X1,X2,X3)) U253(mark(X1),X2,X3) -> mark(U253(X1,X2,X3)) U253(ok(X1),ok(X2),ok(X3)) -> ok(U253(X1,X2,X3)) U254(mark(X1),X2,X3) -> mark(U254(X1,X2,X3)) U254(ok(X1),ok(X2),ok(X3)) -> ok(U254(X1,X2,X3)) U255(mark(X1),X2) -> mark(U255(X1,X2)) U255(ok(X1),ok(X2)) -> ok(U255(X1,X2)) U256(mark(X)) -> mark(U256(X)) U256(ok(X)) -> ok(U256(X)) U261(mark(X1),X2) -> mark(U261(X1,X2)) U261(ok(X1),ok(X2)) -> ok(U261(X1,X2)) U262(mark(X)) -> mark(U262(X)) U262(ok(X)) -> ok(U262(X)) U271(mark(X1),X2) -> mark(U271(X1,X2)) U271(ok(X1),ok(X2)) -> ok(U271(X1,X2)) U272(mark(X)) -> mark(U272(X)) U272(ok(X)) -> ok(U272(X)) U281(mark(X1),X2) -> mark(U281(X1,X2)) U281(ok(X1),ok(X2)) -> ok(U281(X1,X2)) U282(mark(X1),X2) -> mark(U282(X1,X2)) U282(ok(X1),ok(X2)) -> ok(U282(X1,X2)) U291(mark(X1),X2,X3) -> mark(U291(X1,X2,X3)) U291(ok(X1),ok(X2),ok(X3)) -> ok(U291(X1,X2,X3)) U292(mark(X1),X2,X3) -> mark(U292(X1,X2,X3)) U292(ok(X1),ok(X2),ok(X3)) -> ok(U292(X1,X2,X3)) U293(mark(X1),X2,X3) -> mark(U293(X1,X2,X3)) U293(ok(X1),ok(X2),ok(X3)) -> ok(U293(X1,X2,X3)) U294(mark(X1),X2,X3) -> mark(U294(X1,X2,X3)) U294(ok(X1),ok(X2),ok(X3)) -> ok(U294(X1,X2,X3)) U301(mark(X1),X2,X3) -> mark(U301(X1,X2,X3)) U301(ok(X1),ok(X2),ok(X3)) -> ok(U301(X1,X2,X3)) U302(mark(X1),X2) -> mark(U302(X1,X2)) U302(ok(X1),ok(X2)) -> ok(U302(X1,X2)) U303(mark(X1),X2) -> mark(U303(X1,X2)) U303(ok(X1),ok(X2)) -> ok(U303(X1,X2)) U304(mark(X1),X2) -> mark(U304(X1,X2)) U304(ok(X1),ok(X2)) -> ok(U304(X1,X2)) U31(mark(X1),X2,X3) -> mark(U31(X1,X2,X3)) U31(ok(X1),ok(X2),ok(X3)) -> ok(U31(X1,X2,X3)) U311(mark(X1),X2) -> mark(U311(X1,X2)) U311(ok(X1),ok(X2)) -> ok(U311(X1,X2)) U312(mark(X1),X2) -> mark(U312(X1,X2)) U312(ok(X1),ok(X2)) -> ok(U312(X1,X2)) U32(mark(X1),X2,X3) -> mark(U32(X1,X2,X3)) U32(ok(X1),ok(X2),ok(X3)) -> ok(U32(X1,X2,X3)) U321(mark(X1),X2,X3,X4) -> mark(U321(X1,X2,X3,X4)) U321(ok(X1),ok(X2),ok(X3),ok(X4)) -> ok(U321(X1,X2,X3,X4)) U322(mark(X1),X2,X3,X4) -> mark(U322(X1,X2,X3,X4)) U322(ok(X1),ok(X2),ok(X3),ok(X4)) -> ok(U322(X1,X2,X3,X4)) U323(mark(X1),X2,X3,X4) -> mark(U323(X1,X2,X3,X4)) U323(ok(X1),ok(X2),ok(X3),ok(X4)) -> ok(U323(X1,X2,X3,X4)) U324(mark(X1),X2,X3,X4) -> mark(U324(X1,X2,X3,X4)) U324(ok(X1),ok(X2),ok(X3),ok(X4)) -> ok(U324(X1,X2,X3,X4)) U325(mark(X1),X2,X3,X4) -> mark(U325(X1,X2,X3,X4)) U325(ok(X1),ok(X2),ok(X3),ok(X4)) -> ok(U325(X1,X2,X3,X4)) U326(mark(X1),X2,X3,X4) -> mark(U326(X1,X2,X3,X4)) U326(ok(X1),ok(X2),ok(X3),ok(X4)) -> ok(U326(X1,X2,X3,X4)) U327(mark(X1),X2) -> mark(U327(X1,X2)) U327(ok(X1),ok(X2)) -> ok(U327(X1,X2)) U33(mark(X1),X2,X3) -> mark(U33(X1,X2,X3)) U33(ok(X1),ok(X2),ok(X3)) -> ok(U33(X1,X2,X3)) U331(mark(X1),X2,X3) -> mark(U331(X1,X2,X3)) U331(ok(X1),ok(X2),ok(X3)) -> ok(U331(X1,X2,X3)) U332(mark(X1),X2) -> mark(U332(X1,X2)) U332(ok(X1),ok(X2)) -> ok(U332(X1,X2)) U333(mark(X1),X2) -> mark(U333(X1,X2)) U333(ok(X1),ok(X2)) -> ok(U333(X1,X2)) U334(mark(X1),X2) -> mark(U334(X1,X2)) U334(ok(X1),ok(X2)) -> ok(U334(X1,X2)) U34(mark(X1),X2) -> mark(U34(X1,X2)) U34(ok(X1),ok(X2)) -> ok(U34(X1,X2)) U341(mark(X1),X2,X3) -> mark(U341(X1,X2,X3)) U341(ok(X1),ok(X2),ok(X3)) -> ok(U341(X1,X2,X3)) U342(mark(X1),X2,X3) -> mark(U342(X1,X2,X3)) U342(ok(X1),ok(X2),ok(X3)) -> ok(U342(X1,X2,X3)) U343(mark(X1),X2,X3) -> mark(U343(X1,X2,X3)) U343(ok(X1),ok(X2),ok(X3)) -> ok(U343(X1,X2,X3)) U344(mark(X1),X2,X3) -> mark(U344(X1,X2,X3)) U344(ok(X1),ok(X2),ok(X3)) -> ok(U344(X1,X2,X3)) U41(mark(X1),X2,X3) -> mark(U41(X1,X2,X3)) U41(ok(X1),ok(X2),ok(X3)) -> ok(U41(X1,X2,X3)) U42(mark(X1),X2,X3) -> mark(U42(X1,X2,X3)) U42(ok(X1),ok(X2),ok(X3)) -> ok(U42(X1,X2,X3)) U43(mark(X1),X2,X3) -> mark(U43(X1,X2,X3)) U43(ok(X1),ok(X2),ok(X3)) -> ok(U43(X1,X2,X3)) U44(mark(X1),X2,X3) -> mark(U44(X1,X2,X3)) U44(ok(X1),ok(X2),ok(X3)) -> ok(U44(X1,X2,X3)) U45(mark(X1),X2) -> mark(U45(X1,X2)) U45(ok(X1),ok(X2)) -> ok(U45(X1,X2)) U46(mark(X)) -> mark(U46(X)) U46(ok(X)) -> ok(U46(X)) U51(mark(X1),X2,X3) -> mark(U51(X1,X2,X3)) U51(ok(X1),ok(X2),ok(X3)) -> ok(U51(X1,X2,X3)) U52(mark(X1),X2,X3) -> mark(U52(X1,X2,X3)) U52(ok(X1),ok(X2),ok(X3)) -> ok(U52(X1,X2,X3)) U53(mark(X1),X2,X3) -> mark(U53(X1,X2,X3)) U53(ok(X1),ok(X2),ok(X3)) -> ok(U53(X1,X2,X3)) U54(mark(X1),X2,X3) -> mark(U54(X1,X2,X3)) U54(ok(X1),ok(X2),ok(X3)) -> ok(U54(X1,X2,X3)) U55(mark(X1),X2) -> mark(U55(X1,X2)) U55(ok(X1),ok(X2)) -> ok(U55(X1,X2)) U56(mark(X)) -> mark(U56(X)) U56(ok(X)) -> ok(U56(X)) U61(mark(X1),X2) -> mark(U61(X1,X2)) U61(ok(X1),ok(X2)) -> ok(U61(X1,X2)) U62(mark(X1),X2) -> mark(U62(X1,X2)) U62(ok(X1),ok(X2)) -> ok(U62(X1,X2)) U63(mark(X)) -> mark(U63(X)) U63(ok(X)) -> ok(U63(X)) U71(mark(X1),X2) -> mark(U71(X1,X2)) U71(ok(X1),ok(X2)) -> ok(U71(X1,X2)) U72(mark(X1),X2) -> mark(U72(X1,X2)) U72(ok(X1),ok(X2)) -> ok(U72(X1,X2)) U73(mark(X)) -> mark(U73(X)) U73(ok(X)) -> ok(U73(X)) U81(mark(X1),X2) -> mark(U81(X1,X2)) U81(ok(X1),ok(X2)) -> ok(U81(X1,X2)) U82(mark(X1),X2) -> mark(U82(X1,X2)) U82(ok(X1),ok(X2)) -> ok(U82(X1,X2)) U83(mark(X)) -> mark(U83(X)) U83(ok(X)) -> ok(U83(X)) U91(mark(X1),X2) -> mark(U91(X1,X2)) U91(ok(X1),ok(X2)) -> ok(U91(X1,X2)) U92(mark(X1),X2) -> mark(U92(X1,X2)) U92(ok(X1),ok(X2)) -> ok(U92(X1,X2)) U93(mark(X)) -> mark(U93(X)) U93(ok(X)) -> ok(U93(X)) afterNth(X1,mark(X2)) -> mark(afterNth(X1,X2)) afterNth(mark(X1),X2) -> mark(afterNth(X1,X2)) afterNth(ok(X1),ok(X2)) -> ok(afterNth(X1,X2)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) fst(mark(X)) -> mark(fst(X)) fst(ok(X)) -> ok(fst(X)) head(mark(X)) -> mark(head(X)) head(ok(X)) -> ok(head(X)) isLNat(ok(X)) -> ok(isLNat(X)) isLNatKind(ok(X)) -> ok(isLNatKind(X)) isNatural(ok(X)) -> ok(isNatural(X)) isNaturalKind(ok(X)) -> ok(isNaturalKind(X)) isPLNat(ok(X)) -> ok(isPLNat(X)) isPLNatKind(ok(X)) -> ok(isPLNatKind(X)) natsFrom(mark(X)) -> mark(natsFrom(X)) natsFrom(ok(X)) -> ok(natsFrom(X)) pair(X1,mark(X2)) -> mark(pair(X1,X2)) pair(mark(X1),X2) -> mark(pair(X1,X2)) pair(ok(X1),ok(X2)) -> ok(pair(X1,X2)) proper(0()) -> ok(0()) proper(nil()) -> ok(nil()) proper(tt()) -> ok(tt()) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) snd(mark(X)) -> mark(snd(X)) snd(ok(X)) -> ok(snd(X)) splitAt(X1,mark(X2)) -> mark(splitAt(X1,X2)) splitAt(mark(X1),X2) -> mark(splitAt(X1,X2)) splitAt(ok(X1),ok(X2)) -> ok(splitAt(X1,X2)) tail(mark(X)) -> mark(tail(X)) tail(ok(X)) -> ok(tail(X)) take(X1,mark(X2)) -> mark(take(X1,X2)) take(mark(X1),X2) -> mark(take(X1,X2)) take(ok(X1),ok(X2)) -> ok(take(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) - Signature: {U101/3,U102/3,U103/3,U104/3,U105/2,U106/1,U11/3,U111/2,U112/1,U12/3,U121/2,U122/1,U13/3,U131/1,U14/3,U141/1 ,U151/1,U161/1,U171/2,U172/1,U181/2,U182/2,U183/1,U191/2,U192/2,U193/1,U201/3,U202/3,U203/3,U204/3,U205/2 ,U206/1,U21/3,U211/1,U22/3,U221/1,U23/3,U231/2,U232/1,U24/2,U241/3,U242/3,U243/3,U244/3,U245/2,U246/1,U251/3 ,U252/3,U253/3,U254/3,U255/2,U256/1,U261/2,U262/1,U271/2,U272/1,U281/2,U282/2,U291/3,U292/3,U293/3,U294/3 ,U301/3,U302/2,U303/2,U304/2,U31/3,U311/2,U312/2,U32/3,U321/4,U322/4,U323/4,U324/4,U325/4,U326/4,U327/2 ,U33/3,U331/3,U332/2,U333/2,U334/2,U34/2,U341/3,U342/3,U343/3,U344/3,U41/3,U42/3,U43/3,U44/3,U45/2,U46/1 ,U51/3,U52/3,U53/3,U54/3,U55/2,U56/1,U61/2,U62/2,U63/1,U71/2,U72/2,U73/1,U81/2,U82/2,U83/1,U91/2,U92/2,U93/1 ,afterNth/2,cons/2,fst/1,head/1,isLNat/1,isLNatKind/1,isNatural/1,isNaturalKind/1,isPLNat/1,isPLNatKind/1 ,natsFrom/1,pair/2,proper/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,top/1} / {0/0,active/1,mark/1,nil/0,ok/1 ,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {U101,U102,U103,U104,U105,U106,U11,U111,U112,U12,U121,U122 ,U13,U131,U14,U141,U151,U161,U171,U172,U181,U182,U183,U191,U192,U193,U201,U202,U203,U204,U205,U206,U21,U211 ,U22,U221,U23,U231,U232,U24,U241,U242,U243,U244,U245,U246,U251,U252,U253,U254,U255,U256,U261,U262,U271,U272 ,U281,U282,U291,U292,U293,U294,U301,U302,U303,U304,U31,U311,U312,U32,U321,U322,U323,U324,U325,U326,U327,U33 ,U331,U332,U333,U334,U34,U341,U342,U343,U344,U41,U42,U43,U44,U45,U46,U51,U52,U53,U54,U55,U56,U61,U62,U63,U71 ,U72,U73,U81,U82,U83,U91,U92,U93,afterNth,cons,fst,head,isLNat,isLNatKind,isNatural,isNaturalKind,isPLNat ,isPLNatKind,natsFrom,pair,proper,s,sel,snd,splitAt,tail,take,top} and constructors {0,active,mark,nil,ok ,tt} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))